/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.symm;

import java.util.ArrayList;
import java.util.Collections;
import java.util.Comparator;
import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.Set;
import java.util.TreeMap;
import java.util.TreeSet;

import alloy.ast.Leaf;
import alloy.ast.LeafId;
import alloy.ast.Multiplicity;
import alloy.ast.SigExpr;
import alloy.ast.VariableExpr;
import alloy.transl.ASTInfo;
import alloy.transl.ExprTransl;
import alloy.transl.RelationAllocator;
import alloy.type.BasicType;
import alloy.type.RelationType;
import alloy.type.SigType;
import alloy.util.Dbg;

/**
 * Implements special symmetry-breaking for total orders (the std/ord Alloy module).  See that module
 * for explanation of the special symmetry-breaking that we do.
 */
class SBM_Ord extends SymmetryBreakingMethod {
    private static final boolean dbg = false;

    //////////////
    // Methods //
    ////////////

    SBM_Ord(ASTInfo astInfo_, RelationAllocator relAlloc_) {
    super(astInfo_, relAlloc_);
    }

    /**
     * Information about a group of relations that define a total order.
     */
    private static class OrdInfo {
    /** The {@link BasicType} on which the total order is being defined */
    BasicType totallyOrderedType;
    /** The LeafId of the SigExpr corresponding to the static signature Ord */
    LeafId ordId;
    /** The LeafId of the 'next' relation */
    LeafId nextId;
    /** The LeafId of the 'prev' relation */
    LeafId prevId;
    /** The LeafId of the 'first' relation */
    LeafId firstId;
    /** The LeafId of the 'last' relation */
    LeafId lastId;
    }

    SymmetryBreakingPredicate breakSymmetry(AvailableSymmetry availSymm_,
                        Set /* of BasicType */ basicTypes_) {
    SymmetryBreakingPredicate sbp = new SymmetryBreakingPredicate();
    Set /* of BasicType */ totallyOrderedTypes = new TreeSet();

    // Loop through all relations, looking for total order components
    // (fields of Ord[X]) such that X is in basicTypes_ and is fully symmetric.

    /**
     * Map from a BasicType of an Ord signature to the OrdInfo structure for that
     * total order.
     */
    Map /* BasicType -> OrdInfo */ ordSigType2ordInfo = new TreeMap();

    //
    // Get a list of relations sorted by descending arity -- to make sure we see the
    // first/last/next/prev fields before we see the Ord SigExpr during
    // subsequent iteration.
    //
    List /* of LeafId */ rels = new ArrayList(_astInfo.getRelations());
    Collections.sort(rels, new Comparator() {
        public int compare(Object obj1_, Object obj2_) {
            LeafId leafId1 = (LeafId)obj1_;
            LeafId leafId2 = (LeafId)obj2_;
            int arity1 = _astInfo.getLeafType(leafId1).numBasicTypes();
            int arity2 = _astInfo.getLeafType(leafId2).numBasicTypes();
            if (arity1 < arity2) return +1;  // sic
            if (arity1 > arity2) return -1;
            return 0;
        }
        });


    for (Iterator relIter = _astInfo.getRelations().iterator(); relIter.hasNext();) {
        LeafId relId = (LeafId)relIter.next();
        RelationType relType = _astInfo.getLeafType(relId);

        SigType sigType = relType.getSigType();
        //System.out.println("*** sigType=" + sigType.toString());
        if (sigType.toString().endsWith("/Ord")) {
        Dbg.chk(sigType.getSignature().getMult().equals(Multiplicity.ONE));
        Dbg.chk(sigType.getScope()==1);  // because static sig Ord[t] ...
        // the signature should not extend any signature: we don't allow Ord[X] extends Y
        // Dbg.chk(!sigType.getSignature().getExtends().getSigExprIter().hasNext());

        String fieldName = null;
        Leaf leafRep = _astInfo.getLeafRep(relId);
        if (leafRep instanceof VariableExpr)
            fieldName = ((VariableExpr)leafRep).getVar().getId().nodeString();

        OrdInfo ordInfo = (OrdInfo)ordSigType2ordInfo.get(relType.getBasicTypeAt(0));
        if (ordInfo == null)
            ordSigType2ordInfo.put(relType.getBasicTypeAt(0), ordInfo = new OrdInfo());
        if (fieldName==null || fieldName.length()==0) {
            // this is the Ord[X] relation itself, i.e. the
            // SigExpr for the set of atoms of the basic type Ord[X].
            // it is static and contains the one atom.  note that it cannot
            // be a subsignature because currently we do not allow extending
            // an instantiation of a polymorphic signature.
            ordInfo.ordId = relId;
            // have we already seen any fields of this Ord signature?
        }  // this is the Ord[X] relation

        if (fieldName!=null && fieldName.equals("first_")) {
            // this is the Ord[X]$first relation
            ordInfo.firstId = relId;
        }  // this is the Ord[X]$first relation

        if (fieldName!=null && fieldName.equals("last_")) {
            // this is the Ord[X]$last relation
            ordInfo.lastId = relId;
        }  // this is the Ord[X]$last relation
        if (fieldName!=null && fieldName.equals("next_")) {
            // this is the Ord[X]$next relation
            ordInfo.nextId = relId;
        }  // this is the Ord[X]$next relation
        if (fieldName!=null && fieldName.equals("prev_")) {
            // this is the Ord[X]$prev relation
            ordInfo.prevId = relId;
        }  // this is the Ord[X]$prev relation
        }  // this relation is a total order component
    }  // loop over relations

    //
    // Now loop through the OrdInfo's we have build, and break total order symmetries.
    //
    for (Iterator entryIter = ordSigType2ordInfo.entrySet().iterator(); entryIter.hasNext();) {
        Map.Entry entry = (Map.Entry)entryIter.next();
        BasicType ordSigType = (BasicType)entry.getKey();
        OrdInfo ordInfo = (OrdInfo)entry.getValue();
        if(ordInfo.ordId != null &&
           ordInfo.nextId != null &&
           ordInfo.prevId != null &&
           ordInfo.firstId != null &&
           ordInfo.lastId != null) {
        RelationType ordType = _astInfo.getLeafType(ordInfo.ordId);
        RelationType firstType = _astInfo.getLeafType(ordInfo.firstId);
        RelationType lastType = _astInfo.getLeafType(ordInfo.lastId);
        RelationType nextType = _astInfo.getLeafType(ordInfo.nextId);
        RelationType prevType = _astInfo.getLeafType(ordInfo.prevId);
        Dbg.chk(ordType.numBasicTypes() == 1 &&
            firstType.numBasicTypes() == 2 &&
            lastType.numBasicTypes() == 2 &&
            nextType.numBasicTypes() == 3 &&
            prevType.numBasicTypes() == 3);
        Dbg.chk(ordType.getBasicTypeAt(0).equals(ordSigType));
        Dbg.chk(firstType.getBasicTypeAt(0).equals(ordSigType));
        Dbg.chk(lastType.getBasicTypeAt(0).equals(ordSigType));
        Dbg.chk(nextType.getBasicTypeAt(0).equals(ordSigType));
        Dbg.chk(prevType.getBasicTypeAt(0).equals(ordSigType));
        ordInfo.totallyOrderedType = firstType.getBasicTypeAt(1);
        Dbg.chk(firstType.getBasicTypeAt(1).equals(ordInfo.totallyOrderedType));
        Dbg.chk(lastType.getBasicTypeAt(1).equals(ordInfo.totallyOrderedType));
        Dbg.chk(nextType.getBasicTypeAt(1).equals(ordInfo.totallyOrderedType));
        Dbg.chk(nextType.getBasicTypeAt(2).equals(ordInfo.totallyOrderedType));
        Dbg.chk(prevType.getBasicTypeAt(1).equals(ordInfo.totallyOrderedType));
        Dbg.chk(prevType.getBasicTypeAt(2).equals(ordInfo.totallyOrderedType));

        if (basicTypes_.contains(ordInfo.totallyOrderedType) &&
            availSymm_.isFullySymmetric(ordInfo.totallyOrderedType)) {

            //System.out.println("breaking total order symmetry on basic type " + ordInfo.totallyOrderedType);

            ExprTransl ordTransl = _relAlloc.getRelationTransl(ordInfo.ordId);
            sbp.require(ordTransl.getTupleFormula(0), true);

            int orderedTypeScope = ordInfo.totallyOrderedType.getScope();

            ExprTransl firstTransl = _relAlloc.getRelationTransl(ordInfo.firstId);
            for (int atom=0; atom<orderedTypeScope; atom++)
            sbp.require(firstTransl.getTupleFormula(0, atom), atom==0);

            ExprTransl lastTransl = _relAlloc.getRelationTransl(ordInfo.lastId);
            for (int atom=0; atom<orderedTypeScope; atom++)
            sbp.require(lastTransl.getTupleFormula(0, atom),
                    atom == orderedTypeScope-1);

            ExprTransl nextTransl = _relAlloc.getRelationTransl(ordInfo.nextId);
            for (int atom1=0; atom1<orderedTypeScope; atom1++)
            for (int atom2=0; atom2<orderedTypeScope; atom2++)
                sbp.require(nextTransl.getTupleFormula(0, atom1, atom2),
                    atom2 == atom1+1);

            ExprTransl prevTransl = _relAlloc.getRelationTransl(ordInfo.prevId);
            for (int atom1=0; atom1<orderedTypeScope; atom1++)
            for (int atom2=0; atom2<orderedTypeScope; atom2++)
                sbp.require(prevTransl.getTupleFormula(0, atom1, atom2),
                    atom2 == atom1-1);

            availSymm_.removeAllSymmetry(ordInfo.totallyOrderedType);

            // for this ordered type, let's find its SigExpr and force its translation to
            // univ[X] (i.e. to array of TRUE).  this is the unfortunate side effect
            // of instantiating Ord[X]: it imposes a constraint "univ[X] in X" on X.
            // see the text of the module std/ord for more info.

            int foundRels = 0;
            for (Iterator relIter = _astInfo.getRelations().iterator(); relIter.hasNext();) {
            LeafId relId = (LeafId)relIter.next();
            RelationType relType = _astInfo.getLeafType(relId);
            SigType sigType = relType.getSigType();
            Leaf leafRep = _astInfo.getLeafRep(relId);
            if (relType.numBasicTypes() == 1 &&
                relType.getBasicTypeAt(0).equals(ordInfo.totallyOrderedType) &&
                // important: check that this SigExpr represents the top-level SigExpr of the
                // basic type with which the signature was instantiated --
                // and not some subsignature of the same basic type
                sigType.toExpr().nodeString().equals(leafRep.nodeString())) {
                Dbg.chk(leafRep instanceof SigExpr);
                Dbg.chk(sigType.toExpr().nodeString().equals(leafRep.nodeString()));
                ExprTransl relTransl = _relAlloc.getRelationTransl(relId);
                for (int atom=0; atom<sigType.getScope(); atom++)
                sbp.conjoin(relTransl.getTupleFormula(atom));
                foundRels++;
            }  // the relation is the SigExpr for X where Ord[X] was instantiated
            }  // loop over relations
            Dbg.chk(foundRels == 1);
        }  // we should break symmetry on this totally ordered type

        }
    }   // loop over OrdInfo entries we have computed

    return sbp;
    }  // breakSymmetry()
}  // class SBM_Ord



